es:ES, e1, e2:E, P:({e:E| loc(e) = loc(e1)  Id }Prop).
loc(e2) = loc(e1)  Id  e[e1,e2).P(e)  Prop 

latex

Definitions	t  T, b, P  Q, False, A, x:A. B(x), P & Q, (e <loc e'), loc(e), Id, ES, E, Prop, x(s), e  e' , e[e1,e2).P(e)
Lemmas	es-le wf, es-locl wf, es-E wf, event system wf, Id wf, es-loc wf, es-le-loc, es-loc-pred